Quick start: verifying C code using Frama-C/Codex

1. Download the latest binary release of Frama-C/Codex at https://github.com/codex-semantics-library/codex/releases/

2. Write a small C function in file test.c:

   int main(int i) { int x = i; if(i > 8) x = 8; return x; }

   If GCC is not installed, use test.i instead of test.c (.i corresponds to already-preprocessed files).

3. Launch the analysis and obtain a textual report of the analysis:

   $ frama_c_codex -codex test.c -codex-exp-dump -main main
   [kernel] Parsing test.c (with preprocessing)
   [Codex_config] Setting pointer size to 64
   $ cat main.cdump
   test.c:1.26-27: `i' -> [--..--]
   test.c:1.32-37: `i > 8' -> {0; 1}
   test.c:1.32-33: `i' -> [--..--]
   test.c:1.53-54: `x' -> [-0x80000000..8]
   Unproved regular alarms:
   Unproved additional alarms:
   Proved 0/0 regular alarms
   Unproved 0 regular alarms and 0 additional alarms.
   Solved 0/0 user assertions, proved 0

   If you are using Emacs' compilation-mode (probably works also in other editors), you can click on each expression, and they will bring you to the location in the file.

4. Obtain an HTML report of the analysis:

   $ frama_c_codex -codex test.c -main main -codex-html-dump
   ...

5. That's all to get started! As there are no reported alarms, your code is memory-safe, free from division-by-zero errors, and free from others errors that Codex checks. The most useful options are:

   • -codex launches Codex;
   • -main selects the entry point of the analysis;
   • -codex-exp-dump produces a textual dump of all expressions funcname.cdump;
   • -codex-html-dump produces an HTML equivalent of the dump file;
   • -codex-type-file file.typedc uses TypedC specification, useful when analyzing functions independently, which is covered by the types tutorial

Happy verification!